YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { @([](), xs) -> xs
  , @(::(x, xs), ys) -> ::(x, @(xs, ys))
  , flatten([]()) -> []()
  , flatten(::(x, xs)) -> @(x, flatten(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(@) = {2}, Uargs(::) = {2}
TcT has computed following constructor-restricted linear polynomial
interpretation.
       [[]]() = 0            
                             
  [@](x1, x2) = 1 + 2*x1 + x2
                             
 [::](x1, x2) = 2 + x1 + x2  
                             
[flatten](x1) = 1 + 2*x1     
                             

This order satisfies following ordering constraints

         [@([](), xs)] = 1 + xs             
                       > xs                 
                       = [xs]               
                                            
    [@(::(x, xs), ys)] = 5 + 2*x + 2*xs + ys
                       > 3 + x + 2*xs + ys  
                       = [::(x, @(xs, ys))] 
                                            
       [flatten([]())] = 1                  
                       >                    
                       = [[]()]             
                                            
  [flatten(::(x, xs))] = 5 + 2*x + 2*xs     
                       > 2 + 2*x + 2*xs     
                       = [@(x, flatten(xs))]
                                            

Hurray, we answered YES(?,O(n^1))